chain-consistent(f;chain)
== (e:E(Sys). no_repeats(Id;chain(e)) & (0 < ||chain(e)||) & (loc(e)  chain(e)))
== & (e, e':E(Sys). chain(e)  chain(e')  chain(e')  chain(e))
== & (e:E(Sys).
== & ((((e  In))  (loc(e) = if isupdate(In(e)) then hd((chain(e))) else last(chain(e)) fi ))
== & (& ((((e  In)))
== & (& ( ((loc(f(e)) = loc(e)))
== & (& ( (adjacent(Id;chain(e);loc(f(e));loc(e)) & adjacent(Id;chain(f(e));loc(f(e));loc(e))))
== & (& ((((e  In)))  (loc(f(e)) = loc(e))  (a:E(Sys). (a <loc e)  a loc f(e) ))
== & (& (((e  Out))  (loc(e) = last(chain(e)))))
== & (e, e':E(Sys). (e <loc e')  chain(e')  chain(e)) 

latex

---

clarification:

chain-consistent(es;Sys;In;isupdate;Out;f;chain)
== (e:es-E-interface(es;Sys).
== (no_repeats(Id;chain(e)) & (0 < ||chain(e)||) & (es-loc(es; e)  chain(e)  Id))
== & (e:es-E-interface(es;Sys), e':es-E-interface(es;Sys).
== & (sublist(Id; (chain(e)); (chain(e')))  sublist(Id; (chain(e')); (chain(e))))
== & (e:es-E-interface(es;Sys).
== & ((((e  In))
== & (( (es-loc(es; e) = if isupdate(In(e)) then hd((chain(e))) else last(chain(e)) fi   Id))
== & (& ((((e  In)))
== & (& ( ((es-loc(es; (f(e))) = es-loc(es; e)  Id))
== & (& ( (adjacent(Id;chain(e);es-loc(es; (f(e)));es-loc(es; e))
== & (& ( & adjacent(Id;chain(f(e));es-loc(es; (f(e)));es-loc(es; e))))
== & (& ((((e  In)))
== & (& ( (es-loc(es; (f(e))) = es-loc(es; e)  Id)
== & (& ( (a:es-E-interface(es;Sys). es-locl(es; a; e)  es-le(es;a;f(e))))
== & (& (((e  Out))  (es-loc(es; e) = last(chain(e))  Id)))
== & (e:es-E-interface(es;Sys), e':es-E-interface(es;Sys).
== & (es-locl(es; e; e')  sublist(Id; (chain(e')); (chain(e)))) 

latex

Up	abstract chain replication
Wellformedness Lemmas	chain-consistent wf
Definitions	no_repeats(T;l), a < b, #$n, ||as||, (x  l), P  Q, if b then t else f fi , X(e), hd(l), P & Q, adjacent(T;L;x;y), A, e loc e' , b, e  X, s = t, loc(e), last(L), x:A. B(x), E(X), P  Q, (e <loc e'), L1  L2, Id, f(a)
FDL editor aliases	chain-consistent